Tute (Week 10)
Table of Contents
1 Church Numerals
This question will use the Church encoding of the natural numbers, as seen in the lectures. Here's a quick refresher:
\begin{array}{rcl} 0 & = & \lambda f\ x.\ x \\ 1 & = & \lambda f\ x.\ f\ x \\ 2 & = & \lambda f\ x.\ f(f\ x) \\ \dots & & \\ & & \\ (+) & = & \lambda n\ m\ f \ x.\ n\ f\ (m\ f\ x) \end{array}- You might expect that \((+)\) is commutative, in the sense that \((+)\ a\ b\) and \((+)\ b\ a\) reduce to the same value for all \(a\) and \(b\). That is not the case. Can you think of a counterexample? Hint: try feeding it things that aren't Church numerals.
- How would you define multiplication of Church numerals in the lambda calculus?
- How would you define exponentiation?
How would you define the predecessor function on Church numerals? In day-to-day mathematics this function could be defined as
\begin{array}{lcll} pre(0) & = & 0 \\ pre(n) & = & n - 1 & \quad\mbox{if } n > 0 \end{array}Where the fist clause is to prevent us from falling outside the natural numbers. This is sometimes called saturating subtraction.
This question is harder than the rest. You may want to save it for last.
- Given a predecessor function as defined in the previous question, can you define saturating subtraction (where \(n - m = 0\) if \(m > n\))?
Can you define a function which, given two numbers, returns \(\mathsf{true}\) iff they are equal?
Recall the Church encoding of the booleans:
\begin{array}{rcl} \mathsf{true} & = & \lambda x\ y.\ x \\ \mathsf{false} & = & \lambda x\ y.\ y \end{array}
- We have \[(+)\ (\lambda f\ x.\ f)\ (\lambda f\ x.\ x\ x) \quad\mapsto_\beta^\star\quad \lambda f\ x.\ f\] but if we commute the arguments we get \[(+)\ (\lambda f\ x.\ x\ x)\ (\lambda f\ x.\ f) \quad\mapsto_\beta^\star\quad \lambda f\ x.\ f\ f\]
- \((*) = \lambda n\ m.\ n\ ((+)\ m)\ 0\)
- \(exp = \lambda n\ m.\ m\ ((*)\ n)\ 1\)
\(pre = \lambda n\ f\ x.\ (n\ (\lambda m\ g. g\ (m\ f))\ (\lambda g.\ x))\ (\lambda x.\ x)\)
What's going on here? The intention is that the innermost expression \(n\ (\lambda m\ g. g\ (m\ f))\ (\lambda g.\ x)\) is a copy of the numeral \(n\ f\ x\), but with the outermost \(f\) abstracted. This will evaluate to an expression of the form \(\lambda g. f^{n-1}\ x\). Instantiating \(g\) to be the identity function yields the predecessor of \(n\), as desired.
- \((-) = \lambda n\ m. m\ pre\ n\)
\(\lambda n\ m.\ ((-)\ n\ m)\ (\lambda x.\ \mathsf{false})\ (((-)\ m\ n)\ (\lambda x.\ \mathsf{false})\ \mathsf{true})\)
The idea is that \(n\) equals \(m\) holds iff \(n - m = 0\) and \(m - n = 0\).
2 Fixpoint combinators
We briefly saw Turing's fixpoint combinator in the lectures, a lambda-calculus term which we will denote \(\mu\). Its exact definition is not important right now: what matters is that it satisfies \[\mu\ f \mapsto_\beta^* f(\mu\ f)\]
- Use \(\mu\) to define a function which computes the n:th triangular number.
- Use \(\mu\) to define a function which computes the n:th Fibonacci number.
Hint: your function should take the form \(\mu\ f\) for some \(f\) that you'll have to write. Your \(f\) will be a function that takes two arguments: the first argument represents a continuation (intuitively, a function that you can call to initiate a recursive call) and the second argument will be the number \(n\). You may find it helpful to use the auxiliary functions from the previous question.
\(\mu\ (\lambda c\ n.\ (eq\ n\ 0)\ 0\ ((+)\ n\ (c\ (pre\ n))))\)
This is reminiscent of the following recursive function definition:
\begin{array}{l} c(n) = \\ \quad \mathbf{if}\ n = 0\ \mathbf{then} \\ \qquad 0 \\ \quad\mathbf{else} \\ \qquad n + c(n-1) \end{array}\(\mu\ (\lambda c\ n.\ (eq\ n\ 0)\ 0\ ((eq\ n\ 1)\ 1\ ((+)\ (c\ (pre\ (pre\ n)))\ (c\ (pre\ n)))))\)
This is reminiscent of the following recursive function definition:
\begin{array}{l} c(n) = \\ \quad \mathbf{if}\ n = 0\ \mathbf{then} \\ \qquad 0 \\ \quad \mathbf{else\ if}\ n = 1\ \mathbf{then} \\ \qquad 1 \\ \quad\mathbf{else} \\ \qquad c(n-2) + c(n-1) \end{array}